Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    x - 0  → x
2:    0 - s(y)  → 0
3:    s(x) - s(y)  → x - y
4:    lt(x,0)  → false
5:    lt(0,s(y))  → true
6:    lt(s(x),s(y))  → lt(x,y)
7:    if(true,x,y)  → x
8:    if(false,x,y)  → y
9:    div(x,0)  → 0
10:    div(0,y)  → 0
11:    div(s(x),s(y))  → if(lt(x,y),0,s(div(x - y,s(y))))
There are 6 dependency pairs:
12:    s(x) -# s(y)  → x -# y
13:    LT(s(x),s(y))  → LT(x,y)
14:    DIV(s(x),s(y))  → IF(lt(x,y),0,s(div(x - y,s(y))))
15:    DIV(s(x),s(y))  → LT(x,y)
16:    DIV(s(x),s(y))  → DIV(x - y,s(y))
17:    DIV(s(x),s(y))  → x -# y
The approximated dependency graph contains 3 SCCs: {12}, {13} and {16}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.02 seconds)   ---  May 4, 2006